i, x:Id, k:Knd, ds:x:Id fp Type, da:a:Knd fp Type, f:(State(ds)Valtype(da;k)ds(x)?Void).
@i: with declarations ds:dsda:daeffect of k(v) is x := f s v  Dsys 

latex

Definitions	Dsys, @i: with declarations ds:dsda:daeffect of k(v) is x := f s v, if b t else f fi, eqof(d), MsgA, with declarations ds:dsda:daeffect of k(v) is x := f s v, , State(ds), Valtype(da;k), f(x)?z, IdDeq, a:A fp B(a), x:A. B(x), x. t(x), Knd, t  T, Id
Lemmas	Id wf, Knd wf, fpf wf, id-deq wf, fpf-cap wf, ma-valtype wf, ma-state wf, ma-empty wf, ma-single-effect wf, msga wf, eqof wf, ifthenelse wf